#include "SimulatedAnnealing.h"
#include "TimeElapsed.h"
#include <sys/stat.h>
#include <sstream>

SimulatedAnnealing::SimulatedAnnealing(void)
{
}

std::vector<int> SimulatedAnnealing::initializeNumbers(std::string numbersString, int &numberOfLiterals)
{
        std::cout << "Initializing literals....." << std::endl;

        std::vector<char> vectorCharacters;
        std::vector<std::string> vectorString;
        std::vector<int> vectorNumbers;
        std::string stringNumbers = "";
        int counter = 2;
        int counterSpace = 0;
        int helpCounter = 0;

        for(int i = 0; i < numbersString.length(); i++)
        {
                while(numbersString[i] == '0' && numbersString[i - 1] == ' ')
                {
                        helpCounter++;

                        //"#"
                        if(numbersString[i - counter] == '#')
                        {
                                vectorCharacters.push_back(numbersString[i - 1]);
                                counter = 2;
                                break;
                        }

                        //"  0"
                        if(numbersString[i - counter] == '0' && numbersString[i - counter - 1] == ' ')
                        {
                                vectorCharacters.push_back(numbersString[i - 1]);
                                counter = 2;
                                break;
                        }

                        if(helpCounter == 1)
                        {
                                vectorCharacters.push_back(numbersString[i]);
                                vectorCharacters.push_back(numbersString[i - 1]);
                        }

                        else
                        {
                                vectorCharacters.push_back(numbersString[i - counter]);
                                counter++;
                        }
                }
                helpCounter = 0;
                counter = 2;
        }

        //Char -> string
        for(int i = 0; i < vectorCharacters.size(); i++)
        {
                if(vectorCharacters[i] == ' ')
                        counterSpace++;

                //Found a space
                if(counterSpace == 1)
                {
                        vectorString.push_back(stringNumbers);

                        stringNumbers = "";
                        counterSpace = 0;
                }

                if(vectorCharacters[i] != ' ')
                        stringNumbers += vectorCharacters[i];
        }

        //Reverse the string numbers properly
        for(int i = 0; i < vectorString.size(); i++)
                std::reverse(vectorString[i].begin(), vectorString[i].end());

        //Convert to integer values
        for(int i = 0; i < vectorString.size(); i++)
        {
                if(vectorString[i] != "")
                        vectorNumbers.push_back(atoi(vectorString[i].c_str()));
        }

        //Push in the last number (ending number 0)
        vectorNumbers.push_back(0);

        //Get the number of literals
        numberOfLiterals = vectorNumbers.size();

        return vectorNumbers;
}

void SimulatedAnnealing::initializeDataStructure(std::vector<std::string> &vectorStringNumbers, std::vector<int> vectorNumbers, std::multimap<std::string, std::vector<std::string>> &multiMapLiteralClause)
{
        std::cout << "Initializing data structure....." << std::endl << std::endl;

        std::string clause = "";
        std::string stringLiteral = "";
        std::vector<std::string> vectorClause;

        //Create a vector string numbers
        for(int i = 0; i < vectorNumbers.size(); i++)
        {
                char sizeNumber = (char)vectorNumbers[i];
                char buffer[sizeof(sizeNumber)/sizeof(char) + 10];
                std::string stringNumber = itoa(vectorNumbers[i], buffer, 10);

                if(stringNumber == "0")
                        vectorStringNumbers.push_back("|");
                else
                        vectorStringNumbers.push_back(stringNumber);                            
        }

        //Remove the first "|"
        vectorStringNumbers.erase(vectorStringNumbers.begin());

        for(int i = 0; i < vectorStringNumbers.size(); i++)
        {
                if(vectorStringNumbers[i] == "|")
                {
                        if(clause[clause.length() - 1] == ' ')
                                clause.erase(clause.length() - 1);

                        for(int j = 0; j < clause.length(); j++)
                        {
                                if(clause[j] != ' ')
                                        stringLiteral += clause[j];

                                if(clause[j] == ' ' || j == clause.length() - 1)
                                {
                                        if(stringLiteral != "")
                                        {
                                                //Insert literal and its vector clause into map
                                                multiMapLiteralClause.insert(std::pair<std::string, std::vector<std::string>>(stringLiteral, vectorClause));
                                        }

                                        //Reset
                                        stringLiteral = "";
                                }
                        }

                        //Reset
                        clause = "";

                        //Reset
                        vectorClause.clear();
                }

                else if(vectorStringNumbers[i] != "|")
                {
                        vectorClause.push_back(vectorStringNumbers[i]);
                        clause += vectorStringNumbers[i];
                        clause += " ";
                }
        }
}

int SimulatedAnnealing::randomAssignValuesAndEvaluateSolution(std::ofstream &foutput, std::vector<std::string> &vectorAllClauses, std::vector<std::string> &vectorUnsatisfiedClauses, std::string numberOfXLiterals, std::vector<std::string> &vectorStringNumbers, int numberOfLiterals, std::string numberOfClauses, std::map<std::string, bool> &mapLiteralValues, std::multimap<std::string, bool> &mapClauseValues, clock_t begin)
{
        const int NUMBER_OF_LITERALS = atoi(numberOfXLiterals.c_str());
        const int NUMBER_OF_CLAUSES = atoi(numberOfClauses.c_str());
        std::string satisfaction = "";
        int bestSoFar = 0;
        int randomIndex = 0;
        bool literalValues[2] = {true, false};
        std::string stringLiteral = "";
        std::vector<std::string> vectorCheckedClauses;

        //Iterator vector, to help find elements
        std::vector<std::string>::iterator iteratorVectorString;

        std::cout << "Assigning the literals TRUE/FALSE values randomly....." << std::endl << std::endl;

        //Assign the literals random TRUE/FALSE values
        for(int i = 1; i <= NUMBER_OF_LITERALS; i++)
        {
                char sizeTemp = (char)i;
                char bufferTemp[sizeof(sizeTemp)/sizeof(char) + 10];
                stringLiteral = itoa(i, bufferTemp, 10);

                randomIndex = rand () % 2;
                mapLiteralValues[stringLiteral] = literalValues[randomIndex];

                //Opposite literal value
                int tempLiteral = i * -1;
                sizeTemp = (char)tempLiteral;
                bufferTemp[sizeof(sizeTemp)/sizeof(char) + 10];
                stringLiteral = itoa(tempLiteral, bufferTemp, 10);

                if(randomIndex == 0)
                        mapLiteralValues[stringLiteral] = literalValues[randomIndex + 1];
                else
                        mapLiteralValues[stringLiteral] = literalValues[randomIndex - 1];
        }

        //Assign TRUE/FALSE values to the SAT formula
        std::cout << "Assigning TRUE/FALSE values to the clauses of the SAT formula....." << std::endl << std::endl;

        int trueClauseCounter = 0;
        int trueCounter = 0;
        std::string stringClause = "";

        for(int j = 0; j < vectorStringNumbers.size(); j++)
        {
                if(vectorStringNumbers[j] != "|")
                {
                        stringClause += vectorStringNumbers[j];
                        stringClause += " ";

                        if(mapLiteralValues[vectorStringNumbers[j]] == true)
                                trueCounter++;
                }
                                
                else if(vectorStringNumbers[j] == "|")
                {
                        //Erase the space at the end of string
                        stringClause.erase(stringClause.end() - 1);

                        iteratorVectorString = std::find(vectorCheckedClauses.begin(), vectorCheckedClauses.end(), stringClause);

                        if(iteratorVectorString == vectorCheckedClauses.end())
                        {
                                vectorCheckedClauses.push_back(stringClause);
								vectorAllClauses.push_back(stringClause);

                                if(trueCounter >= 1)
                                {
                                        //Set the clause to TRUE
                                        mapClauseValues.insert(std::pair<std::string, bool>(stringClause, true));
                                        trueClauseCounter++;
                                }
                                                
                                else if(trueCounter == 0)
                                {
                                        //Set the clause to FALSE
                                        mapClauseValues.insert(std::pair<std::string, bool>(stringClause, false));
                                        vectorUnsatisfiedClauses.push_back(stringClause);
                                }                               
                        }

                        //Reset
                        stringClause = "";
                        trueCounter = 0;
                }
        }

        bestSoFar = trueClauseCounter;

        //Reset
        trueClauseCounter = 0;
        vectorCheckedClauses.clear();

        foutput << "Literals: " << numberOfXLiterals << "  Clauses: " << NUMBER_OF_CLAUSES << "\n\n";
        std::cout << "Mean number of TRUE clauses (initial solution): " << std::endl << std::endl << bestSoFar << std::endl << std::endl;
		foutput << "Mean number of TRUE clauses (initial solution): " << std::endl << std::endl << bestSoFar << std::endl << std::endl;

        if(bestSoFar == NUMBER_OF_CLAUSES)
        {
                satisfaction = "SATISFIED";
                std::cout << "SAT with " << numberOfXLiterals << " literals and " <<  NUMBER_OF_CLAUSES << " clauses is " << satisfaction << "." << std::endl << std::endl;
        }
        else
        {
                satisfaction = "NOT SATISFIED";
                std::cout << "SAT with " << numberOfXLiterals << " literals and " <<  NUMBER_OF_CLAUSES << " clauses is " << satisfaction << "." << std::endl << std::endl;
        }

        //Finished!
        if(satisfaction == "SATISFIED")
        {
                system("pause");
                system("exit");
        }

        return bestSoFar;
}

void SimulatedAnnealing::run(std::ofstream &foutput, std::string noLettersCollectionString, int &numberOfLiterals, std::vector<std::string> vectorStringNumbers, std::map<std::string, bool> &mapLiteralValues, std::multimap<std::string, bool> &mapClauseValues, std::string numberOfXLiterals, std::string numberOfClauses, std::multimap<std::string, std::vector<std::string>> &multiMapLiteralClause, clock_t begin)
{
        const int NUMBER_OF_CLAUSES = atoi(numberOfClauses.c_str());    //Number of clauses
		const int NUMBER_OF_LITERALS = atoi(numberOfXLiterals.c_str());
		std::vector<int> vectorLiterals;                                                                //Vector contains literals
        std::vector<int> vectorVisitedLiterals;                                         //Vector contains visited literals
        std::vector<std::string> vectorClauseLiterals;                                 //Vector contains unvisited literals from unsatisfied clause
        std::map<int, int> mapTabuList;                                                                 //Map contains tabu list
        std::map<int, int> mapBestLiterals;                                                             //Map contains best literals
		std::vector<std::string> tempVector;
		std::vector<std::string> vectorClause;
		std::vector<std::string> vectorClauses;
        std::vector<std::string> vectorUnsatisfiedClauses;
		std::vector<std::string> vectorAllClauses;
        bool yesNo[2] = {true, false};
        double flipCounter = 0;
        double powerCounter = 1;
		int helpVariable = 1;
		int trueLiteralCounter = 0;
		int trueClauseCounter = 0;
		std::string stringClause = "";
		std::string stringLiteral = "";			    
		std::string tempStringLiteral = "";
		std::string tempStringLiteral2 = "";
		std::string clause = "";
		std::string satisfaction = "";

        std::pair<std::multimap<std::string, std::vector<std::string>>::iterator, std::multimap<std::string, std::vector<std::string>>::iterator> multiMapIterator;        

        /**Initialize literals**/
        std::vector<int> vectorNumbers = initializeNumbers(noLettersCollectionString, numberOfLiterals);

        /**Initialize data structure**/
        initializeDataStructure(vectorStringNumbers, vectorNumbers, multiMapLiteralClause);

        //Assign TRUE/FALSE values to the SAT formula
        std::cout << "Running Simulated Annealing....." << std::endl << std::endl;        

        //Iterator vector, to help find visited literals
        std::vector<int>::iterator iteratorVector;

        //Iterator vector, to help find elements
        std::vector<std::string>::iterator iteratorVectorString;

        //Iterator vector, to help find elements
        std::vector<int>::iterator iteratorVectorIndex;

        //Iterator map, to help find elements
        std::map<std::string, bool>::iterator iteratorMap;

        //Total iteration time
        double maxIterationTime = 900;
        double totalIterationTime = 0;

        //Object to calculate time
        TimeElapsed te;
		
		/**Random assign TRUE/FALSE values and evaluate initial solution**/
		int satisfiedClauses = randomAssignValuesAndEvaluateSolution(foutput, vectorAllClauses, vectorUnsatisfiedClauses, numberOfXLiterals, vectorStringNumbers, numberOfLiterals, numberOfClauses, mapLiteralValues, mapClauseValues, begin);
		int previousGain = NUMBER_OF_CLAUSES - satisfiedClauses;

		/**CALCULATE TEMPERATURE**/
		double temperature = 0;
		int sum = 0;
		int counter = 0;		
		int newGain = 0;
		int average = 0;    

		for(int i = 0; i < 10000; i++){
			//Pick a random clause
			stringClause = vectorAllClauses[rand() % NUMBER_OF_CLAUSES];
			
			//Pick a random literal
			for(int i = 0; i < stringClause.length(); i++)
			{
					if(stringClause[i] == ' ' || i == stringClause.length() - 1)
					{
							if(stringClause[i] != ' ' && i == stringClause.length() - 1)
									stringLiteral += stringClause[i];

							if(atoi(stringLiteral.c_str()) < 0)
							{
									int temp = atoi(stringLiteral.c_str()) * -1;
									char sizeTempOpposite = (char)temp;
									char bufferTempOpposite[sizeof(sizeTempOpposite)/sizeof(char) + 10];
									std::string oppositeLiteral = itoa(temp, bufferTempOpposite, 10);
									stringLiteral = oppositeLiteral;
							}

							vectorClauseLiterals.push_back(stringLiteral);

							//Reset
							stringLiteral = "";
					}
					else
						stringLiteral += stringClause[i];
			}

			std::random_shuffle(vectorClauseLiterals.begin(), vectorClauseLiterals.end());
			stringLiteral = vectorClauseLiterals[0];

			//Flip literal
			flip(mapLiteralValues, stringLiteral);			

			//std::cout << "Calculating gains....." << std::endl << std::endl;
        
			//Put in tempVector
			tempVector.push_back(stringLiteral);

			//Opposite value
			int oppositeLiteral = atoi(stringLiteral.c_str()) * -1;

			//int -> string
			char sizeTemp = (char)oppositeLiteral;
			char bufferTemp[sizeof(sizeTemp)/sizeof(char) + 10];
                                
			std::string oppositeStringLiteral = itoa(oppositeLiteral, bufferTemp, 10);

			//Put in tempVector
			tempVector.push_back(oppositeStringLiteral);

			//Find the clauses that have this literal and update number of true clauses found
			for(int j = 0; j < tempVector.size(); j++)
			{
					tempStringLiteral2 = tempVector[j];

					//Find the clauses that have this literal
					multiMapIterator = multiMapLiteralClause.equal_range(tempStringLiteral2);

					//Check each clause
					for(std::multimap<std::string, std::vector<std::string>>::iterator multiMapIterator2 = multiMapIterator.first; multiMapIterator2 != multiMapIterator.second; ++multiMapIterator2)
					{
						//Next clause
						vectorClause = (*multiMapIterator2).second;

						//Reset
						clause = "";
                
						//Check if the clause has been handled already
						for(int i = 0; i < vectorClause.size(); i++)
						{
									clause += vectorClause[i];
									clause += " ";
						}

						if(clause[clause.length() - 1] == ' ')
								clause.erase(clause.length() - 1);

						iteratorVectorString = std::find(vectorClauses.begin(), vectorClauses.end(), clause);

						//Not found, handle it
						if(iteratorVectorString == vectorClauses.end())
						{
								clause = "";

								for(int i = 0; i < vectorClause.size(); i++)
								{
											tempStringLiteral = vectorClause[i];

											//Check this literal
											iteratorVectorString = std::find(tempVector.begin(), tempVector.end(), tempStringLiteral);

											if(mapLiteralValues[tempStringLiteral] == true && iteratorVectorString != tempVector.end())
													helpVariable *= 1;

											else if(mapLiteralValues[tempStringLiteral] == true && iteratorVectorString == tempVector.end())
													helpVariable *= 0;
                                        
											else if(mapLiteralValues[tempStringLiteral] == false && iteratorVectorString != tempVector.end())
													helpVariable *= 0;
                                        
											else if(mapLiteralValues[tempStringLiteral] == false && iteratorVectorString == tempVector.end())
													helpVariable *= 1;

											if(mapLiteralValues[tempStringLiteral] == true)
													trueLiteralCounter++;

											clause += tempStringLiteral;
											clause += " ";
								}

								if(clause[clause.length() - 1] == ' ')
										clause.erase(clause.length() - 1);
                                
								vectorClauses.push_back(clause);
                        
								if(trueLiteralCounter == 0)
                                        trueClauseCounter--;

								if(helpVariable == 1)
										trueClauseCounter++;

								//Reset
								helpVariable = 1;

								//Reset
								trueLiteralCounter = 0;
						}
					}
			}

			satisfiedClauses += trueClauseCounter;

			//Set the gain
			newGain = NUMBER_OF_CLAUSES - satisfiedClauses;

			//Clear
			tempVector.clear();

			//Reset
			vectorClause.clear();

			//Reset
			vectorClauses.clear();

			//Reset
			tempStringLiteral = "";

			//Reset
			tempStringLiteral2 = "";

			//Reset
			clause = "";

			//Reset
			trueClauseCounter = 0;

			//Reset
			stringLiteral = "";

			if(newGain > previousGain) {
			sum += (newGain - previousGain);
			counter++;
			}			
		}

		average = sum/counter;
		temperature = average/log(0.5);
		temperature *= -1;
		
		//NUM of unsatisfied clauses
		satisfiedClauses = randomAssignValuesAndEvaluateSolution(foutput, vectorAllClauses, vectorUnsatisfiedClauses, numberOfXLiterals, vectorStringNumbers, numberOfLiterals, numberOfClauses, mapLiteralValues, mapClauseValues, begin);
		previousGain = NUMBER_OF_CLAUSES - satisfiedClauses;
		int bestGain = previousGain;
		int previousBestGain = bestGain;
		newGain = 0;
		int deltaCost = 0;

		foutput << "Mean satisfied clauses     Mean time     Mean flips     Mean temperature\n\n";

		while(temperature > 0.001) {
			//Start time of iteration
            clock_t beginIterationTime = clock();

			for(int i = 0; i < NUMBER_OF_LITERALS; i++) {
				//Pick a random clause
				stringClause = vectorAllClauses[rand() % NUMBER_OF_CLAUSES];
			
				//Pick a random literal
				for(int i = 0; i < stringClause.length(); i++)
				{
						if(stringClause[i] == ' ' || i == stringClause.length() - 1)
						{
								if(stringClause[i] != ' ' && i == stringClause.length() - 1)
										stringLiteral += stringClause[i];

								if(atoi(stringLiteral.c_str()) < 0)
								{
										int temp = atoi(stringLiteral.c_str()) * -1;
										char sizeTempOpposite = (char)temp;
										char bufferTempOpposite[sizeof(sizeTempOpposite)/sizeof(char) + 10];
										std::string oppositeLiteral = itoa(temp, bufferTempOpposite, 10);
										stringLiteral = oppositeLiteral;
								}

								vectorClauseLiterals.push_back(stringLiteral);

								//Reset
								stringLiteral = "";
						}
						else
								stringLiteral += stringClause[i];
				}

				std::random_shuffle(vectorClauseLiterals.begin(), vectorClauseLiterals.end());
				stringLiteral = vectorClauseLiterals[0];

				//Flip literal
				flip(mapLiteralValues, stringLiteral);

				flipCounter++;

				//std::cout << "Calculating gains....." << std::endl << std::endl;
        
				//Put in tempVector
				tempVector.push_back(stringLiteral);

				//Opposite value
				int oppositeLiteral = atoi(stringLiteral.c_str()) * -1;

				//int -> string
				char sizeTemp = (char)oppositeLiteral;
				char bufferTemp[sizeof(sizeTemp)/sizeof(char) + 10];
                                
				std::string oppositeStringLiteral = itoa(oppositeLiteral, bufferTemp, 10);

				//Put in tempVector
				tempVector.push_back(oppositeStringLiteral);

				//Find the clauses that have this literal and update number of true clauses found
				for(int j = 0; j < tempVector.size(); j++)
				{
						tempStringLiteral2 = tempVector[j];

						//Find the clauses that have this literal
						multiMapIterator = multiMapLiteralClause.equal_range(tempStringLiteral2);

						//Check each clause
						for(std::multimap<std::string, std::vector<std::string>>::iterator multiMapIterator2 = multiMapIterator.first; multiMapIterator2 != multiMapIterator.second; ++multiMapIterator2)
						{
							//Next clause
							vectorClause = (*multiMapIterator2).second;

							//Reset
							clause = "";
                
							//Check if the clause has been handled already
							for(int i = 0; i < vectorClause.size(); i++)
							{
										clause += vectorClause[i];
										clause += " ";
							}

							if(clause[clause.length() - 1] == ' ')
									clause.erase(clause.length() - 1);

							iteratorVectorString = std::find(vectorClauses.begin(), vectorClauses.end(), clause);

							//Not found, handle it
							if(iteratorVectorString == vectorClauses.end())
							{
									clause = "";

									for(int i = 0; i < vectorClause.size(); i++)
									{
												tempStringLiteral = vectorClause[i];

												//Check this literal
												iteratorVectorString = std::find(tempVector.begin(), tempVector.end(), tempStringLiteral);

												if(mapLiteralValues[tempStringLiteral] == true && iteratorVectorString != tempVector.end())
														helpVariable *= 1;

												else if(mapLiteralValues[tempStringLiteral] == true && iteratorVectorString == tempVector.end())
														helpVariable *= 0;
                                        
												else if(mapLiteralValues[tempStringLiteral] == false && iteratorVectorString != tempVector.end())
														helpVariable *= 0;
                                        
												else if(mapLiteralValues[tempStringLiteral] == false && iteratorVectorString == tempVector.end())
														helpVariable *= 1;

												if(mapLiteralValues[tempStringLiteral] == true)
														trueLiteralCounter++;

												clause += tempStringLiteral;
												clause += " ";
									}

									if(clause[clause.length() - 1] == ' ')
											clause.erase(clause.length() - 1);
                                
									vectorClauses.push_back(clause);
										                    
									if(trueLiteralCounter == 0)
                                        trueClauseCounter--;

									if(helpVariable == 1)
										trueClauseCounter++;

									//Reset
									helpVariable = 1;

									//Reset
									trueLiteralCounter = 0;
							}
						}
				}

				satisfiedClauses += trueClauseCounter;

				//Set the gain
				newGain = NUMBER_OF_CLAUSES - satisfiedClauses;

				deltaCost = newGain - previousGain;			

				//Clear
				tempVector.clear();

				//Reset
				vectorClause.clear();

				//Reset
				vectorClauses.clear();

				//Reset
				tempStringLiteral = "";

				//Reset
				tempStringLiteral2 = "";

				//Reset
				clause = "";

				//Reset
				trueClauseCounter = 0;

				//Reset
				stringLiteral = "";

				if(newGain <= previousGain) {
					previousGain = newGain;
				}

				else if(newGain > previousGain) {
					int randomNum = rand() % 1;

					if(exp(-deltaCost/-temperature) < randomNum) {		
						//Flip back
						flip(mapLiteralValues, stringLiteral);											
					}
				}	

				if(newGain < bestGain) {
					bestGain = newGain;
				}

				if(NUMBER_OF_CLAUSES - previousGain == NUMBER_OF_CLAUSES)
					break;
			}

			temperature *= 0.95;					

			//End time of iteration
            clock_t endIterationTime = clock();

			//Update total iteration time
            totalIterationTime += te.GetTimeElapsed(endIterationTime, beginIterationTime) / 1000;     

			if(bestGain < previousBestGain) {
				std::cout << NUMBER_OF_CLAUSES - bestGain << std::endl;
				foutput << NUMBER_OF_CLAUSES - bestGain << "                         " << totalIterationTime << "                         " << flipCounter << "                         " << temperature << "\n";			
				previousBestGain = bestGain;
			}

			if(NUMBER_OF_CLAUSES - previousGain == NUMBER_OF_CLAUSES || totalIterationTime >= maxIterationTime)
				break;
		}

		if(NUMBER_OF_CLAUSES - previousGain == NUMBER_OF_CLAUSES)
        {
                satisfaction = "SATISFIED";
				std::cout << "SAT with " << NUMBER_OF_LITERALS << " literals and " <<  NUMBER_OF_CLAUSES << " clauses is " << satisfaction << "." << std::endl << std::endl;
				foutput << "SAT with " << NUMBER_OF_LITERALS << " literals and " <<  NUMBER_OF_CLAUSES << " clauses is " << satisfaction << "." << std::endl << std::endl;
        }
        else
        {
                satisfaction = "NOT SATISFIED";
                std::cout << "SAT with " << NUMBER_OF_LITERALS << " literals and " <<  NUMBER_OF_CLAUSES << " clauses is " << satisfaction << "." << std::endl << std::endl;
				foutput << "SAT with " << NUMBER_OF_LITERALS << " literals and " <<  NUMBER_OF_CLAUSES << " clauses is " << satisfaction << "." << std::endl << std::endl;
		}

		//Show time elapsed
        std::cout << "Time elapsed: " << totalIterationTime << " seconds" << std::endl << std::endl;
        foutput << "Time elapsed: " << totalIterationTime << " seconds\n\n";
}

void SimulatedAnnealing::flip(std::map<std::string, bool> &mapLiteralValues, std::string stringLiteral)
{       
        //std::cout << "Flipping....." << std::endl << std::endl;

        //Flip TRUE to FALSE
        if(mapLiteralValues[stringLiteral] == true)
        {
                //Flip cluster to FALSE
                mapLiteralValues[stringLiteral] = false;

                //Opposite literal value to TRUE
                int temp = atoi(stringLiteral.c_str()) * -1;
                char sizeTempOpposite = (char)temp;
                char bufferTempOpposite[sizeof(sizeTempOpposite)/sizeof(char) + 10];
                std::string oppositeTempLiteral = itoa(temp, bufferTempOpposite, 10);

                mapLiteralValues[oppositeTempLiteral] = true;
        }
                
        //Flip FALSE to TRUE
        else
        {
                //Flip cluster to TRUE
                mapLiteralValues[stringLiteral] = true;

                //Opposite literal value to FALSE
                int temp = atoi(stringLiteral.c_str()) * -1;
                char sizeTempOpposite = (char)temp;
                char bufferTempOpposite[sizeof(sizeTempOpposite)/sizeof(char) + 10];
                std::string oppositeTempLiteral = itoa(temp, bufferTempOpposite, 10);

                mapLiteralValues[oppositeTempLiteral] = false;
        }
}

SimulatedAnnealing::~SimulatedAnnealing(void)
{
}

